Per
TL;DR Фірмовий синтаксис Групоїд Інфініті для Mini-TT/Rust MLTT ядра в нормальній формі Бакуса-Наура для LR(1) парсер генераторів загалом, і Menhir/OCaml та LALRPOP/Rust зокрема.
CoC-88
Name: String = { r"[a-zA-Z_][a-zA-Z_\d]*" => <>.to_string() };
Variable: Per = { <n:Name> => Per::Var(n), };
Universe: Per = { <n:r"\*[\d]+"> => Per::Type(u32::from_str_radix(&n[1..],10).unwrap()),
<n:r"\*"> => Per::Type(0), };
Lambda: Henk = { "(" <v:Name> ":" <t:Expr> ")" <e:Expr1> =>
Henk::Lambda(v,Box::new(t),Box::new(e)) };
Forall: Henk = { "[" <v:Name> ":" <t:Expr> "]" <e:Expr1> =>
Henk::Forall(v,Box::new(t),Box::new(e)) };
// LR(1) Parsing Scheme
Expr1: Henk = { Lambda, Forall, Expr2 };
Expr2: Henk = { <l:Expr2> <r:Expr3> => Henk::App(Box::new(l),Box::new(r)), Expr3 };
Expr3: Henk = { Variable, Universe, <l:"("> <e:Expr1> <r:")"> => e };
pub Expr: Henk = { Expr1 };
MLTT-72
Name: String = { r"[a-zA-Z_][a-zA-Z_\d]*" => <>.to_string() };
Variable: Per = { <n:Name> => Per::Var(n), };
Universe: Per = { <n:r"\*[\d]+"> => Per::Type(u32::from_str_radix(&n[1..],10).unwrap()),
<n:r"\*"> => Per::Type(0), };
Vars: Vec<Pattern> = {
<n:Name> => vec![Pattern::Var(n)],
<n:Name> <v:Vars> =>
{ let mut r = v.clone();
r.append(&mut vec![Pattern::Var(n)]); r }, };
Telescope: Vec<(Pattern,Expression)> = {
"(" <v:Vars> <m:":"> <t:Expr> ")" => vec![(v[0].clone(),t)],
"(" <v:Vars> <m:":"> <t:Expr> ")" <x:Telescope> =>
{ let mut r = x.clone(); r.append(&mut vec![(v[0].clone(),t)]); r } };
Lambda: Per = { "λ" "(" <v:Vars> <m:":"> <t:Expr> ")" <c:","> <e:Exp1> =>
Per::Lambda(v[0].clone(),None,Box::new(e)), };
Forall: Per = { "Π" "(" <v:Vars> <m:":"> <t:Expr> ")" <c:","> <e:Exp1> =>
Per::Pi(Typed::new(v[0].clone(),t), Box::new(e)), };
Sigma: Per = { "Σ" "(" <v:Vars> <m:":"> <t:Expr> ")" <c:","> <e:Exp1> =>
Per::Sigma(Typed::new(v[0].clone(),t), Box::new(e)), };
Exp1: Per = { Lambda, Forall, Sigma, Exp2 };
Exp2: Per = { <l:Exp2> <r:Exp3> => Per::Application(Box::new(l),Box::new(r)), Exp3 };
Exp3: Per = { Universe, Variable, <l:"("> <e:Exp4> <r:")"> => e, };
Exp4: Per = { <l:Exp1> "," <r:Exp4> => Per::Pair(Box::new(l),Box::new(r)), Exp1 };
pub Expr: Per = { Exp1 };
Еволюція синтаксису
Основні лямбла синтаксиси описані були тут.
// ULC = V | ( V : ULC ) ULC | ULC ULC | ( ULC ) -- λ
// AUT = V | ( V : AUT ) AUT | AUT AUT | ( AUT ) -- λ
// | U | [ V : AUT ] AUT -- Π
// PER = V | ( V : PER ) PER | PER PER | ( PER ) -- λ
// | U | [ V : PER ] PER | -- Π
// | { V : PER } PER | PER , PER | PER .1 | PER .2 -- Σ
ULC — це синтаксис нетипизованого лямбда-числення. AUT — це синтаксис одночасно і мови з однією аксіомою AUTOMATH Ніколаса де Брьойна 1968 року, а пізніше і синтаксис для Calculus of Construction Жерара Юе і його учня Тері Кокана 1988 року, а PER — це MLTT синтаксис для ΠΣ-мови Пера Мартіна-Льофа 1972 року.
Для тих, хто вивчає теорію типів, вправи з написання Π-прувера і ΠΣ-прувера є обов'язковими. Просто Агдою навчитися гратися замало.
Ці синаксис представлені у загальній формі, таку форму зазвичай промислові парсер генератори не приймають, а тільки на комбінаторах чи PEG парсерах. Промислові парсер-генератори приймають БНФ граматики написані у LL(1), LR(1), LALR(1) та інших більш strict формах. Найстарійша і найпопулярніша форма LR(1), яка заглядає на один токен вправо і вліво була вибрана як основа для синтаксисів вищих мов Групоїд Інфініті. За основу лямбда сиснтаксиса була взята мова Lean від Microsoft.
Мій учень попросив мене специфікувати ці синтаксис і зробити максимально зрозумілими для Rust програмістів, тому ми взяли LALRPOP, який є канонічним LR(1) парсер-генератором і написали на ньому спочатку CoC-88, а потім MLTT-72.
Наступною вправою після PTS тайпчекера має стати лямбда ліфтінг телескопів і багатозмінність в лінзах. Потім потрібно відірватися від Mini-TT і перейти на свій фірмовий тайпчекер.
Чому ці вправи важливі? Тому, що лямбда числення вищих порядків є внутрішньою мовою локальних декартово-замкнених категорій, і як кажуть поза очі головні дослідники області є природньою формою мислення. За тисячі років людської думки ми не придумали до цих пір більш зручних логік які б не вбудовувалися в цей тайпчекер, більше того, всі мови всіх математик теж зводяться до "для всіх x: A, виконується предикат P(x)" і "існує таке x: A, що виконується предикат P(x)", перше Π або ∀, друге Σ або Ǝ.
Проблеми Гьоделівської нескінченності і обмеження першої теореми про неповноту стосується по-перше систем першого порядку, по-друге аплікейбл до обмеженої кількості аксіом. Предикативні математичні тайпчекери вищих порядків мають нескінченну кількість всесвітів навіть для одного типу, тому теж можуть містити метациркулярні доведення і гомотопічні транспорти одних візерунків в інші, власне вся магія відбувається при доведенні цих ізоморфізмів.
Фінальною точкою, коли людська думка змогла формалізувати мову математики у повному обсязі, не залишивши поза собою жодної теореми, яку не можна було би верифікувати механістично, став 2017 рік з виходом експериментального тайпчекера cubicaltt, який пізніше влився в Agda 2.6 і з тих пір є головним обчислювальним ядром, основного гомотопічного прувера планети.
Існує тільки три інституції в світі які утримують кубічну думку і розуміння як влаштовані ці тайпчекери:
1) Університет Карнегі-Меллона, Піттсбург, США — 🇺🇸 ;
2) Технічний університет Чалмерса, Гетеборг, Швеція — 🇸🇪 ;
3) Політехніка Сікорського, Київ, Україна — 🇺🇦 .
Відповідь на питання чому саме така конструкція є нормальною формою мислення дається в курсі алгебраїчної топології, теорії розшарувань, та в 2.3 параграфі підручнику HoTT. Також Сергій Максименко з НАН України давав публічну вступну лекцію на цю тему.
Я назавжди залишуся людиною, яка принесла гомотопічну теорію типів в Україну і побудувала свою школу і свою лінію виробництва артефіктів (лабораторію).